T:Type, P:(T), L, L1, L2:T List.
interleaving(T;L1;L2;L)  interleaving(T;filter(P;L1);filter(P;L2);filter(P;L)) 

latex

Definitions	t  T, x:A. B(x), , filter(P;l), interleaving(T;L1;L2;L), P & Q, P  Q, P  Q, P  Q, A & B, P  Q, ||as||, tl(l), Prop, False, A, AB, l[i], hd(l), i<j, ij, {T}, SQType(T), b, b, Unit
Lemmas	cons interleaving2, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, cons interleaving, tl wf, select wf, length wf2, length wf1, interleaving of cons, nil interleaving, interleaving of nil, interleaving wf, filter wf, bool wf